00100	GIVEAX(INTSET, ISSET I0);
00200	
00300	GIVEAX(SUCC,(∀ X)(XεI0 ⊃ SUCC(X)εI0));
00400	
00500	GIVEAX(INT0,0εI0);
00600	
00700	GIVEAX(PRED,(∀ X)(XεI0∧¬(X=0)⊃PRED(X)εI0));
00800	
00900	GIVEAX(SN0,(∀ X)(XεI0 ⊃ ¬(SUCC(X)=0)));
01000	
01100	GIVEAX(PS,(∀ X)(XεI0 ⊃ X = PRED SUCC X));
01200	
01300	GIVEAX(SP,(∀ X)(XεI0∧¬(X=0) ⊃ X = SUCC PRED X));
01400	
01500	GIVEAX(INDUCTION,(∀ U)(U ⊂ I0 ∧ 0εU ∧ (∀ X)(XεU ⊃ SUCC(X)εU)
01600		⊃ U=I0));
01700	
01800	GIVEAX(PLUSS,(∀ X)(∀ Y)(XεI0∧YεI0 ⊃((Y=0)⊃X+Y=X)
01900	∧(¬(Y=0)⊃X+Y=SUCC(X)+PRED(Y))));
02000	
02100	GIVEAX(LESS,(∀ X)(∀ Y)(XεI0∧YεI0 ⊃
02150		(X<Y ≡ Y≠0 ∧(X=0 ∨ PRED X < PRED Y))));
02200	
02300	GIVEAX(THLESS,LEε(I0→(I0→TV)) ∧
02400		(∀ X)(∀ Y)(XεI0∧YεI0 ⊃ (X<Y ≡ ββ(X,LE,Y))));
     

00100	END;